| Definitions |  b, P   Q,  x:A. B(x), P & Q, Top, t  T, IdDeq, Id, Type,  x.A(x),  x:A. B(x),  x. t(x), f(x)?z, x:A  B(x), S  T, State(ds), State(ds), tag(k), Void, <a,b>, s = t, DeclaredType(ds;x), type List, x:A B(x), S  T, isrcv(k), lnk(k), IdLnk, Prop, source(l), destination(l), es realizer ind Rsends compseq tag def, R-Feasible(R), A & B, Possible(R;es), es realizer ind Reffect compseq tag def, @i: only members of L read x, @i:k sends only on links in L, @i: k affects only L, @i Precondition for a(v)P State(ds) (v:T), sends k(v:T) on l:tagged(g,State(ds),v):dt, @i events of kind k change x to f State(ds) (val:T), only events in L send on l with tg, @i only events in L change x : T, @i x initially v:T, es realizer ind Rrframe compseq tag def, [[R]], es realizer ind Rbframe compseq tag def, es realizer ind Raframe compseq tag def, es realizer ind Rpre compseq tag def, es realizer ind Rsframe compseq tag def, es realizer ind Rframe compseq tag def, es realizer ind Rinit compseq tag def, @loc: only members of L read x, D realizes es. P(es), ES, @loc: k sends only on links in L, @loc: k writes only members of L, @loc precondition for a(v:T):P State(ds) v, Case b of inl(x) s(x) ; inr(y) t(y), if b t else f fi, sends knd(v:T) on l:tagged(g,State(ds),v):dt, @loc effect knd(v:T) x := f State(ds) v , only events in L send on lnk with tag, @loc only events in L change x:T, @loc x initially v:T, True, Consistent(R;es), {T}, es realizer ind Rplus compseq tag def, es realizer ind Rnone compseq tag def, left  right,  , left+right, Unit, Knd, a:A fp B(a), rec(x.A(x)), Realizer, P  Q, P Q |